<!DOCTYPE html>
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
<title>test.agda</title>
<meta name="generator" content="KF5::SyntaxHighlighting - Definition (Agda) - Theme (Breeze Light)"/>
</head><body style="background-color:#ffffff;color:#1f1c1b"><pre>
<span style="color:#898887;">-- Agda Sample File</span>
<span style="color:#898887;">-- https://github.com/agda/agda/blob/master/examples/syntax/highlighting/Test.agda</span>

<span style="color:#898887;">-- This test file currently lacks module-related stuff.</span>

<span style="color:#898887;">{- Nested</span>
<span style="color:#898887;">   {- comment. -} -}</span>

<span style="font-weight:bold;">module</span> Test <span style="font-weight:bold;">where</span>

<span style="font-weight:bold;">infix</span>  <span style="color:#b08000;">12</span> <span style="color:#006e28;">_</span>!
<span style="font-weight:bold;">infixl</span>  <span style="color:#b08000;">7</span> <span style="color:#006e28;">_</span>+<span style="color:#006e28;">_</span> <span style="color:#006e28;">_</span>-<span style="color:#006e28;">_</span>
<span style="font-weight:bold;">infixr</span>  <span style="color:#b08000;">2</span> -<span style="color:#006e28;">_</span>

<span style="font-weight:bold;">postulate</span> x <span style="color:#006e28;">:</span> <span style="color:#0057ae;">Set</span>

f <span style="color:#006e28;">:</span> <span style="color:#006e28;">(</span><span style="color:#0057ae;">Set</span> <span style="color:#006e28;">-&gt;</span> <span style="color:#0057ae;">Set</span> <span style="color:#006e28;">-&gt;</span> <span style="color:#0057ae;">Set</span><span style="color:#006e28;">)</span> <span style="color:#006e28;">-&gt;</span> <span style="color:#0057ae;">Set</span>
f <span style="color:#006e28;">_</span>*<span style="color:#006e28;">_</span> <span style="color:#006e28;">=</span> x * x

<span style="font-weight:bold;">data</span> ℕ <span style="color:#006e28;">:</span> <span style="color:#0057ae;">Set</span> <span style="font-weight:bold;">where</span>
  zero <span style="color:#006e28;">:</span> ℕ
  suc  <span style="color:#006e28;">:</span> ℕ <span style="color:#006e28;">-&gt;</span> ℕ

<span style="color:#006e28;">_</span>+<span style="color:#006e28;">_</span> <span style="color:#006e28;">:</span> ℕ <span style="color:#006e28;">-&gt;</span> ℕ <span style="color:#006e28;">-&gt;</span> ℕ
zero  + n <span style="color:#006e28;">=</span> n
suc m + n <span style="color:#006e28;">=</span> suc <span style="color:#006e28;">(</span>m + n<span style="color:#006e28;">)</span>

<span style="font-weight:bold;">postulate</span> <span style="color:#006e28;">_</span>-<span style="color:#006e28;">_</span> <span style="color:#006e28;">:</span> ℕ <span style="color:#006e28;">-&gt;</span> ℕ <span style="color:#006e28;">-&gt;</span> ℕ

-<span style="color:#006e28;">_</span> <span style="color:#006e28;">:</span> ℕ <span style="color:#006e28;">-&gt;</span> ℕ
- n <span style="color:#006e28;">=</span> n

<span style="color:#006e28;">_</span>! <span style="color:#006e28;">:</span> ℕ <span style="color:#006e28;">-&gt;</span> ℕ
zero  ! <span style="color:#006e28;">=</span> suc zero
suc n ! <span style="color:#006e28;">=</span> n - n !

<span style="font-weight:bold;">record</span> Equiv <span style="color:#006e28;">{</span>a <span style="color:#006e28;">:</span> <span style="color:#0057ae;">Set</span><span style="color:#006e28;">}</span> <span style="color:#006e28;">(_</span>≈<span style="color:#006e28;">_</span> <span style="color:#006e28;">:</span> a <span style="color:#006e28;">-&gt;</span> a <span style="color:#006e28;">-&gt;</span> <span style="color:#0057ae;">Set</span><span style="color:#006e28;">)</span> <span style="color:#006e28;">:</span> <span style="color:#0057ae;">Set</span> <span style="font-weight:bold;">where</span>
  <span style="font-weight:bold;">field</span>
    refl      <span style="color:#006e28;">:</span> <span style="font-weight:bold;">forall</span> x       <span style="color:#006e28;">-&gt;</span> x ≈ x
    sym       <span style="color:#006e28;">:</span> <span style="color:#006e28;">{</span>x y <span style="color:#006e28;">:</span> a<span style="color:#006e28;">}</span>      <span style="color:#006e28;">-&gt;</span> x ≈ y <span style="color:#006e28;">-&gt;</span> y ≈ x
    <span style="color:#006e28;">_</span>`trans`<span style="color:#006e28;">_</span> <span style="color:#006e28;">:</span> <span style="font-weight:bold;">forall</span> <span style="color:#006e28;">{</span>x y z<span style="color:#006e28;">}</span> <span style="color:#006e28;">-&gt;</span> x ≈ y <span style="color:#006e28;">-&gt;</span> y ≈ z <span style="color:#006e28;">-&gt;</span> x ≈ z

<span style="font-weight:bold;">data</span> <span style="color:#006e28;">_</span>≡<span style="color:#006e28;">_</span> <span style="color:#006e28;">{</span>a <span style="color:#006e28;">:</span> <span style="color:#0057ae;">Set</span><span style="color:#006e28;">}</span> <span style="color:#006e28;">(</span>x <span style="color:#006e28;">:</span> a<span style="color:#006e28;">)</span> <span style="color:#006e28;">:</span> a <span style="color:#006e28;">-&gt;</span> <span style="color:#0057ae;">Set</span> <span style="font-weight:bold;">where</span>
  refl <span style="color:#006e28;">:</span> x ≡ x

subst <span style="color:#006e28;">:</span> <span style="font-weight:bold;">forall</span> <span style="color:#006e28;">{</span>a x y<span style="color:#006e28;">}</span> <span style="color:#006e28;">-&gt;</span>
  <span style="color:#006e28;">(</span>P <span style="color:#006e28;">:</span> a <span style="color:#006e28;">-&gt;</span> <span style="color:#0057ae;">Set</span><span style="color:#006e28;">)</span> <span style="color:#006e28;">-&gt;</span> x ≡ y <span style="color:#006e28;">-&gt;</span> P x <span style="color:#006e28;">-&gt;</span> P y
subst <span style="color:#006e28;">{</span>x <span style="color:#006e28;">=</span> x<span style="color:#006e28;">}</span> <span style="color:#006e28;">.{</span>y <span style="color:#006e28;">=</span> x<span style="color:#006e28;">}</span> <span style="color:#006e28;">_</span> refl p <span style="color:#006e28;">=</span> p

Equiv-≡ <span style="color:#006e28;">:</span> <span style="font-weight:bold;">forall</span> <span style="color:#006e28;">{</span>a<span style="color:#006e28;">}</span> <span style="color:#006e28;">-&gt;</span> Equiv <span style="color:#006e28;">{</span>a<span style="color:#006e28;">}</span> <span style="color:#006e28;">_</span>≡<span style="color:#006e28;">_</span>
Equiv-≡ <span style="color:#006e28;">{</span>a<span style="color:#006e28;">}</span> <span style="color:#006e28;">=</span>
  <span style="font-weight:bold;">record</span> <span style="color:#006e28;">{</span> refl      <span style="color:#006e28;">=</span> <span style="color:#006e28;">\_</span> <span style="color:#006e28;">-&gt;</span> refl
         <span style="color:#006e28;">;</span> sym       <span style="color:#006e28;">=</span> sym
         <span style="color:#006e28;">;</span> <span style="color:#006e28;">_</span>`trans`<span style="color:#006e28;">_</span> <span style="color:#006e28;">=</span> <span style="color:#006e28;">_</span>`trans`<span style="color:#006e28;">_</span>
         <span style="color:#006e28;">}</span>
  <span style="font-weight:bold;">where</span>
  sym <span style="color:#006e28;">:</span> <span style="color:#006e28;">{</span>x y <span style="color:#006e28;">:</span> a<span style="color:#006e28;">}</span> <span style="color:#006e28;">-&gt;</span> x ≡ y <span style="color:#006e28;">-&gt;</span> y ≡ x
  sym refl <span style="color:#006e28;">=</span> refl

  <span style="color:#006e28;">_</span>`trans`<span style="color:#006e28;">_</span> <span style="color:#006e28;">:</span> <span style="color:#006e28;">{</span>x y z <span style="color:#006e28;">:</span> a<span style="color:#006e28;">}</span> <span style="color:#006e28;">-&gt;</span> x ≡ y <span style="color:#006e28;">-&gt;</span> y ≡ z <span style="color:#006e28;">-&gt;</span> x ≡ z
  refl `trans` refl <span style="color:#006e28;">=</span> refl

<span style="font-weight:bold;">postulate</span>
  String <span style="color:#006e28;">:</span> <span style="color:#0057ae;">Set</span>
  Char   <span style="color:#006e28;">:</span> <span style="color:#0057ae;">Set</span>
  Float  <span style="color:#006e28;">:</span> <span style="color:#0057ae;">Set</span>

<span style="font-weight:bold;">data</span> Int <span style="color:#006e28;">:</span> <span style="color:#0057ae;">Set</span> <span style="font-weight:bold;">where</span>
  pos    <span style="color:#006e28;">:</span> ℕ <span style="color:#006e28;">→</span> Int
  negsuc <span style="color:#006e28;">:</span> ℕ <span style="color:#006e28;">→</span> Int

<span style="color:#006e28;">{-# BUILTIN STRING  String #-}</span>
<span style="color:#006e28;">{-# BUILTIN CHAR    Char   #-}</span>
<span style="color:#006e28;">{-# BUILTIN FLOAT   Float  #-}</span>

<span style="color:#006e28;">{-# BUILTIN NATURAL ℕ      #-}</span>

<span style="color:#006e28;">{-# BUILTIN INTEGER       Int    #-}</span>
<span style="color:#006e28;">{-# BUILTIN INTEGERPOS    pos    #-}</span>
<span style="color:#006e28;">{-# BUILTIN INTEGERNEGSUC negsuc #-}</span>

<span style="font-weight:bold;">data</span> [<span style="color:#006e28;">_</span>] <span style="color:#006e28;">(</span>a <span style="color:#006e28;">:</span> <span style="color:#0057ae;">Set</span><span style="color:#006e28;">)</span> <span style="color:#006e28;">:</span> <span style="color:#0057ae;">Set</span> <span style="font-weight:bold;">where</span>
  []  <span style="color:#006e28;">:</span> [ a ]
  <span style="color:#006e28;">_</span>∷<span style="color:#006e28;">_</span> <span style="color:#006e28;">:</span> a <span style="color:#006e28;">-&gt;</span> [ a ] <span style="color:#006e28;">-&gt;</span> [ a ]

<span style="color:#006e28;">{-# BUILTIN LIST [_] #-}</span>
<span style="color:#006e28;">{-# BUILTIN NIL  []  #-}</span>
<span style="color:#006e28;">{-# BUILTIN CONS _∷_ #-}</span>

<span style="font-weight:bold;">primitive</span>
  primStringToList <span style="color:#006e28;">:</span> String <span style="color:#006e28;">-&gt;</span> [ Char ]

string <span style="color:#006e28;">:</span> [ Char ]
string <span style="color:#006e28;">=</span> primStringToList <span style="color:#bf0303;">&quot;∃ apa&quot;</span>

char <span style="color:#006e28;">:</span> Char
char <span style="color:#006e28;">=</span> <span style="color:#924c9d;">'∀'</span>

anotherString <span style="color:#006e28;">:</span> String
anotherString <span style="color:#006e28;">=</span> <span style="color:#bf0303;">&quot;¬ be\</span>
<span style="color:#bf0303;">    \pa&quot;</span>

nat <span style="color:#006e28;">:</span> ℕ
nat <span style="color:#006e28;">=</span> <span style="color:#b08000;">45</span>

float <span style="color:#006e28;">:</span> Float
float <span style="color:#006e28;">=</span> <span style="color:#b08000;">45.0e-37</span>

<span style="color:#898887;">-- Testing qualified names.</span>

<span style="font-weight:bold;">open</span> <span style="font-weight:bold;">import</span> Test
Eq <span style="color:#006e28;">=</span> Test<span style="color:#006e28;">.</span>Equiv <span style="color:#006e28;">{</span>Test<span style="color:#006e28;">.</span>ℕ<span style="color:#006e28;">}</span>
</pre></body></html>
